$\forall$$T$:Type, $f$:($T$$\rightarrow$$T$). retraction($T$;$f$) $\Rightarrow$ ($\forall$$x$:$T$. $\exists$$y$:$T$. ($f$($y$) = $y$ \& $y$ is $f$$\ast$($x$)))